This invention relates generally to microprocessing, and more particularly to providing methods to improve floating point arithmetic operations.
In most processors, it is common to see some type of floating point unit (FPU) or other processing unit that completely implements (or at least has enhanced support for) various floating point divide instructions. Implementations of these instructions are based on popular division algorithms, including non-restoring SRT (Sweeney Robertson Tocher) division, Newton-Raphson division, Goldschmidt division and others.
Errors may occur during execution of these instructions using any of various algorithms, either due to errors in the design (including the algorithm itself) or due to circuit malfunctions such as manufacturing faults or rare environmental disturbances. Functional checking of these types of floating point divide algorithms and their results using formal verification techniques is not currently available, and such checking would only serve to eliminate design flaws, as opposed to malfunctions occurring during execution.
Accordingly, other techniques have been devised to try and verify the correctness of the algorithm and/or the result. For example, previous machines have focused on verifying the internal verifiable mathematical operations of the divide using parity and residue checks. While these techniques can verify the correctness of each internal operation, they do not speak to the correctness of the divide algorithm or final result.
Thus, it would be desirable to be able to detect errors in the final result of a floating point divide algorithm, particularly to detect errors occurring due to a circuit malfunction. Such an ability would be useful in providing a method to verify the actual results of a divide operation without the need to verify each mathematical step in the algorithm.